the_es:event_system{i:l}, e:es-E(the_es). es-valtype(the_es; e)  Type 

latex

Definitions	x:A. B(x), t  T, es-valtype(es; e), if b then t else f fi , P  Q, tt, ff, prop{i:l}, , Unit, P  Q, P  Q,
Lemmas	es-isrcv wf, bool wf, eqtt to assert, es-rcvtype wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, es-acttype wf, es-E wf, event system wf